ePMC

Benchmark
Model:majority v.1 (CTMC)
Parameter(s)T = 2100
Property:change_state (prob-reach-time-bounded)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ./root/epmc-standard.jar check --model-input-files majority.prism --model-input-type prism --property-input-files majority.props --property-input-names change_state --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const T=2100
Execution
Walltime:44.629342794418335s
Return code:0
Relative Error:1.3520154585882968e-08
Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property change_state
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 11498 11498
build-model-states-explored 27219 15721
build-model-states-explored 43688 16469
build-model-states-explored 59791 16103
build-model-states-explored 76156 16365
build-model-states-explored 92721 16565
build-model-states-explored 108742 16021
build-model-states-explored 125353 16611
build-model-states-explored 141130 15777
build-model-states-explored 157967 16837
build-model-states-explored 174981 17014
build-model-done 192000 11
iterating-progress-bounded 223 7350 0.03034013605442177 1
iterating-progress-bounded 479 7350 0.06517006802721088 2
iterating-progress-bounded 732 7350 0.09959183673469388 3
iterating-progress-bounded 986 7350 0.1341496598639456 4
iterating-progress-bounded 1241 7350 0.168843537414966 5
iterating-progress-bounded 1496 7350 0.2035374149659864 6
iterating-progress-bounded 1746 7350 0.23755102040816325 7
iterating-progress-bounded 2001 7350 0.27224489795918366 8
iterating-progress-bounded 2255 7350 0.30680272108843537 9
iterating-progress-bounded 2510 7350 0.3414965986394558 10
iterating-progress-bounded 2765 7350 0.3761904761904762 11
iterating-progress-bounded 3020 7350 0.4108843537414966 12
iterating-progress-bounded 3275 7350 0.445578231292517 13
iterating-progress-bounded 3530 7350 0.48027210884353744 14
iterating-progress-bounded 3785 7350 0.5149659863945578 15
iterating-progress-bounded 4040 7350 0.5496598639455782 16
iterating-progress-bounded 4293 7350 0.5840816326530612 17
iterating-progress-bounded 4547 7350 0.6186394557823129 18
iterating-progress-bounded 4802 7350 0.6533333333333333 19
iterating-progress-bounded 5057 7350 0.6880272108843537 20
iterating-progress-bounded 5305 7350 0.7217687074829932 21
iterating-progress-bounded 5560 7350 0.7564625850340136 22
iterating-progress-bounded 5815 7350 0.791156462585034 23
iterating-progress-bounded 6070 7350 0.8258503401360544 24
iterating-progress-bounded 6324 7350 0.8604081632653061 25
iterating-progress-bounded 6579 7350 0.8951020408163265 26
iterating-progress-bounded 6834 7350 0.929795918367347 27
iterating-progress-bounded 7089 7350 0.9644897959183674 28
iterating-progress-bounded 7344 7350 0.9991836734693877 29
model-checking-done 43
command-check-result-is 0.05429919399413349 change_state